package edu.uic.cs.cs582.process.impl;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.Comparator;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.TreeMap;
import java.util.concurrent.atomic.AtomicInteger;

import org.apache.commons.collections.primitives.ArrayIntList;
import org.apache.commons.collections.primitives.IntList;
import org.apache.commons.lang.StringUtils;

import edu.mit.jwi.item.POS;
import edu.uic.cs.cs582.data.Component;
import edu.uic.cs.cs582.data.Polarity;
import edu.uic.cs.cs582.data.Synset;
import edu.uic.cs.cs582.data.Word;
import edu.uic.cs.cs582.misc.Assert;
import edu.uic.cs.cs582.process.CnfGenerator;
import edu.uic.cs.cs582.process.impl.SatIndexParser.Index;
import edu.uic.cs.cs582.process.impl.SatIndexParser.WordIndex;

public class AddingFrequencyCnfGeneratorImplKeepingMiddleVariables extends
		AbstractVariablesOperations implements CnfGenerator
{
	private static class SortedAddArrayList extends ArrayList<int[]>
	{
		private static final long serialVersionUID = 4289534836450229881L;

		public SortedAddArrayList()
		{
			super();
		}

		@Override
		public boolean add(int[] e)
		{
			Arrays.sort(e);
			return super.add(e);
		}
	}

	public AddingFrequencyCnfGeneratorImplKeepingMiddleVariables(
			Component component)
	{
		super(component);
	}

	@Override
	public Map<int[], Index> generateCnfs(POS pos, Word word, Polarity polarity)
	{
		System.out.println(">>>>>>>>>>>>>>>>>>>>> " + word);

		if (word.getSynsetsNumberRelateTo() == 1
				&& polarity != Polarity.NEUTRAL)
		{
			System.out
					.println("<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<");
			System.out.println();

			return generateCnfForWordHasOnlyOneSynset(word, polarity);
		}

		////////////////////////////////////////////////////////////////////////

		Map<int[], Index> result = new TreeMap<int[], Index>(
				new IntArrayComparator());
		int halfFrequencySum = word.getFrequencySum() / 2;

		AtomicInteger variableIndexBase = new AtomicInteger(0);
		if (polarity != Polarity.NEUTRAL)
		{
			IntList finalFrequencySummationDigits = generateAndStoreCnfsForNonNeutralWord(
					word, polarity, variableIndexBase, result);

			Map<int[], Index> greaterThanHalfExpression = generateCnfForSummationGreaterThanValue(
					word, finalFrequencySummationDigits, halfFrequencySum);
			result.putAll(greaterThanHalfExpression);
		}
		else
		{
			IntList finalPositiveFrequencySummationDigits = generateAndStoreCnfsForNonNeutralWord(
					word, Polarity.POSITIVE, variableIndexBase, result);
			IntList finalNegativeFrequencySummationDigits = generateAndStoreCnfsForNonNeutralWord(
					word, Polarity.NEGATIVE, variableIndexBase, result); // continue using variableIndexBase

			Map<int[], Index> positiveLessThanOrEqualsToHalfExpression = generateCnfForSummationLessThanOrEqualsToValue(
					word, finalPositiveFrequencySummationDigits,
					halfFrequencySum);
			Map<int[], Index> negativeLessThanOrEqualsToHalfExpression = generateCnfForSummationLessThanOrEqualsToValue(
					word, finalNegativeFrequencySummationDigits,
					halfFrequencySum);

			result.putAll(positiveLessThanOrEqualsToHalfExpression);
			result.putAll(negativeLessThanOrEqualsToHalfExpression);
		}

		System.out.println("<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<");
		System.out.println();

		return result;
	}

	/**
	 * If a word has ONLY ONE synset, then you can assume that the frequency is 1. 
	 * The frequency may be whatever 12, 0.1, 30, 10000 in WordNet, we make it 1. 
	 * This does not change the semantics. The synset, because is the only one, 
	 * is the dominant synset regardless of its frequency with respect to the word.
	 * 
	 * when the word is positive is 
	 * [NOT s+, b]
	 * [s+, NOT b]
	 * [b]
	 * 
	 * This formula can be reduced to:
	 * [s+]
	 * [b]
	 * 
	 * Furthermore, since b is a DUMMY vaiable, i.e., 
	 * it does not appear anywhere else, we can drop it. 
	 * So, all we have left as a formula for the word is:
	 * [s+]
	 * 
	 * So, in general for one-synset words we have the formula
	 * [s+] if the word is positive
	 * and the formula
	 * [s-] if the word is negative.
	 * 
	 * @param word
	 * @param polarity 
	 * @return
	 */
	private Map<int[], Index> generateCnfForWordHasOnlyOneSynset(Word word,
			Polarity polarity)
	{
		Synset synset = word.getSynsetsRelateTo().iterator().next();
		int synsetIndexInComponent = component.getIndexOfSynset(synset);
		int[] clause = null;

		//		if (polarity != Polarity.NEUTRAL)
		//		{
		int synsetIndexSymbol = polarSymbol(polarity, synsetIndexInComponent);

		clause = new int[] { synsetIndexSymbol };
		//		}
		//		else
		//		{
		//			int synsetIndexSymbolPositive = polarSymbol(Polarity.POSITIVE,
		//					synsetIndexInComponent);
		//			int synsetIndexSymbolNegative = polarSymbol(Polarity.NEGATIVE,
		//					synsetIndexInComponent);
		//
		//			clause = new int[] { not(synsetIndexSymbolPositive),
		//					not(synsetIndexSymbolNegative) };
		//		}

		System.out.println(word + " has only one synset "
				+ Arrays.toString(clause));
		return Collections.singletonMap(clause,
				(Index) new WordIndex(component.getIndexOfWord(word), -1));
	}

	private IntList generateAndStoreCnfsForNonNeutralWord(Word word,
			Polarity polarity, AtomicInteger variableIndexBase,
			Map<int[], Index> result)
	{
		int initialIndexBase = variableIndexBase.get();
		// stores all the frequency-digit variables for each synset of current word
		LinkedList<IntList> frequencyDigits = new LinkedList<IntList>();

		int wordIndexInComponent = component.getIndexOfWord(word);
		for (Entry<Synset, Integer> frequencyBySynset : word
				.getFrequenciesBySynsetRelateTo().entrySet())
		{
			Synset synset = frequencyBySynset.getKey();
			int frequency = frequencyBySynset.getValue();
			// NOTICE! reverse order!
			String frequencyBinaryString = StringUtils.reverse(Integer
					.toBinaryString(frequency));

			// Step 2, 3
			Map<int[], Index> cnfForOneFrequency = generateCnfForOneNonNeutralFrequency(
					polarity, synset, frequencyBinaryString,
					variableIndexBase.get(), wordIndexInComponent,
					frequencyDigits);
			result.putAll(cnfForOneFrequency);

			variableIndexBase.addAndGet(frequencyBinaryString.length());
		}

		Assert.isTrue(word.getTotalFrequencyDigitNumber() == (variableIndexBase
				.get() - initialIndexBase));
		// step 4
		Map<int[], Index> additionExpression = generateCnfForFrequencyAddition(
				frequencyDigits, word, variableIndexBase);
		result.putAll(additionExpression);

		Assert.isTrue(frequencyDigits.size() == 1);
		// step 5
		IntList finalFrequencySummationDigits = frequencyDigits.poll();
		Assert.isTrue(finalFrequencySummationDigits.size() >= Integer
				.toBinaryString(word.getFrequencySum()).length());

		return finalFrequencySummationDigits;
	}

	/**
	 * 
	 *  -------------------------
	 * |Step 2 and 3 in my report|
	 *  -------------------------
	 *  
	 *
	 * Suppose w1 is POSITIVE 
	 * and one synset s1’s frequency is 6 = (110)_bin.
	 *
	 *	   (s1+ -> (x12=1) AND (x11=1) AND (x10=0))
	 * AND (¬s1+ -> (x12=0) AND (x11=0) AND (x10=0)
	 * 	
	 * ⇔      (¬s1+ OR (x12 AND x11 AND ¬x10))
	 * AND (s1+ OR (¬x12 AND ¬x11 AND ¬x10))
	 * 
	 * ⇔      (¬s1+ OR ¬x10)
	 * AND (¬s1+ OR x11)
	 * AND (¬s1+ OR x12)
	 * 
	 * AND (s1+ OR ¬x10)
	 * AND (s1+ OR ¬x11) 
	 * AND (s1+ OR ¬x12)
	 * 
	 * ⇔      (¬s1+ OR ¬x10)
	 * AND (s1+ OR ¬x10)
	 * 
	 * AND (¬s1+ OR x11)
	 * AND (s1+ OR ¬x11) 
	 * 
	 * AND (¬s1+ OR x12)
	 * AND (s1+ OR ¬x12)
	 * 
	 */
	private Map<int[], Index> generateCnfForOneNonNeutralFrequency(
			Polarity wordPolarity, Synset synset, String frequencyBinaryString,
			int variableIndexBase, int wordIndexInComponent,
			List<IntList> frequencyDigits)
	{
		int synsetIndexInComponent = component.getIndexOfSynset(synset);

		Map<int[], Index> result = new HashMap<int[], Index>(
				frequencyBinaryString.length());
		/*SynsetAndWordIndex synsetAndWordIndex = new SynsetAndWordIndex(
				synsetIndexInComponent, wordIndexInComponent);*/
		WordIndex wordIndex = new WordIndex(wordIndexInComponent, -1);

		////////////////////////////////////////////////////////////////////////
		// store all the indices for each digit of a frequency for current word 
		IntList frequencyDigitIndices = new ArrayIntList(
				frequencyBinaryString.length());
		// put the frequency digits for one synset of a current word
		frequencyDigits.add(frequencyDigitIndices);
		////////////////////////////////////////////////////////////////////////

		// s1+
		int synsetIndexSymbol = polarSymbol(wordPolarity,
				synsetIndexInComponent);
		// ¬s1+
		int synsetNotIndexSymbol = not(synsetIndexSymbol);
		int length = frequencyBinaryString.length() + variableIndexBase;
		int[] clause = null;

		for (int variableIndex = variableIndexBase; variableIndex < length; variableIndex++)
		{
			// x11
			int frequencyDigitVariableSymbol = frequencyDigitSymbol(
					variableIndex, wordIndexInComponent);
			System.out.println("frequency bit for " + synset + " ~ "
					+ frequencyDigitVariableSymbol);

			// store this digit ////////////////////////////////////////////////
			frequencyDigitIndices.add(frequencyDigitVariableSymbol);
			////////////////////////////////////////////////////////////////////

			// ¬x11
			int frequencyDigitVariableSymbolNotSymbol = not(frequencyDigitVariableSymbol);

			//  (¬s1+ OR ¬x10)
			if (frequencyBinaryString.charAt(variableIndex - variableIndexBase) == '0')
			{
				clause = generateSynsetORVariableClause(synsetNotIndexSymbol,
						frequencyDigitVariableSymbolNotSymbol);
				result.put(clause, wordIndex/*synsetAndWordIndex*/);
			}
			// (¬s1+ OR x11)
			else
			{
				clause = generateSynsetORVariableClause(synsetNotIndexSymbol,
						frequencyDigitVariableSymbol);
				result.put(clause, wordIndex/*synsetAndWordIndex*/);
			}

			// (s1+ OR ¬x10) || (s1+ OR ¬x11) 
			clause = generateSynsetORVariableClause(synsetIndexSymbol,
					frequencyDigitVariableSymbolNotSymbol);
			result.put(clause, wordIndex/*synsetAndWordIndex*/);

		}

		System.out.println("Step 2 " + synset + " ["
				+ StringUtils.reverse(frequencyBinaryString)
				+ "]======================");
		for (int[] each : result.keySet())
		{
			System.out.println(Arrays.toString(each));
		}
		System.out.println("Step 2 ==========================================");

		return result;
	}

	private int[] generateSynsetORVariableClause(int synsetIndexSymbol,
			int variableSymbol)
	{
		int[] clause = new int[2];

		// Remember in sorted order
		if (variableSymbol > synsetIndexSymbol)
		{
			clause[0] = synsetIndexSymbol;
			clause[1] = variableSymbol;
		}
		else
		{
			clause[0] = variableSymbol;
			clause[1] = synsetIndexSymbol;
		}

		return clause;
	}

	////////////////////////////////////////////////////////////////////////////

	/**
	 *  -------------------
	 * |Step 4 in my report|
	 *  -------------------
	 *  
	 * @param frequencyDigitsQueue initially it stores digit variables for each frequency
	 * @param nextDigitIndex index for the next generating variable,
	 *  which may be carrier or summation digit
	 * @return
	 */
	private Map<int[], Index> generateCnfForFrequencyAddition(
			LinkedList<IntList> frequencyDigitsQueue, Word word,
			AtomicInteger nextDigitIndex)
	{
		// ordered by size in order to let those two with same size process first, 
		// and hence reduce the number of variables. e.g.,
		//     abc : def = 3; hijk : lmno = 4; 3 : 4 = 4 ; total = 3+4+4 = 11
		// BUT, abc : hijk = 4;  def: lmno = 4; 4 : 4 = 4; total = 4+4+4 = 12
		Comparator<IntList> queueSizeSorter = new Comparator<IntList>()
		{
			@Override
			public int compare(IntList o1, IntList o2)
			{
				// order by size
				return o1.size() - o2.size();
			}
		};
		Collections.sort(frequencyDigitsQueue, queueSizeSorter);
		////////////////////////////////////////////////////////////////////////

		int wordIndexInComponent = component.getIndexOfWord(word);
		WordIndex wordIndex = new WordIndex(wordIndexInComponent, -1);

		/**
		 * 					x_i+1	x_i	...	x_1	x_0
		 * 			y_i+2	y_i+1	y_i	...	y_1	y_0
		 * ----------------------------------------
		 * c_i+3	c_i+2	c_i+1	c_i	...	c_1	 /
		 * s_i+3	s_i+2	s_i+1	s_i	...	s_1	s_0
		 */
		Map<int[], Index> result = new TreeMap<int[], Index>(
				new IntArrayComparator());

		IntList first = null;
		IntList second = null;
		while ((first = frequencyDigitsQueue.poll()) != null)
		{
			if ((second = frequencyDigitsQueue.poll()) != null)
			{
				Assert.isTrue(!first.isEmpty());
				Assert.isTrue(!second.isEmpty());

				IntList frequencySummationDigits = new ArrayIntList(
						second.size() + 1);

				// second's size always >= first since they have been sorted
				// For carries: 	  1, 2, 3, ..., sizeOfFirst ~ total sizeOfFirst
				// For summations: 0, 1, 2, 3, ..., ..., ..., sizeOfSecond ~ total (sizeOfSecond+1)
				int c_previous = 0;
				int c_current = 0;
				for (int index = 0; index < (second.size() + 1); index++)
				{
					if (index != 0)
					{
						// c_i
						c_current = frequencyDigitSymbol(
								nextDigitIndex.getAndIncrement(),
								wordIndexInComponent);
						System.out.println("carry for " + word.getWord()
								+ " ~ " + c_current);
						generateAndStoreCarries(index, first, second,
								c_previous, c_current, wordIndex, result);
						c_previous = c_current;
					}

					//s_i
					int s_current = frequencyDigitSymbol(
							nextDigitIndex.getAndIncrement(),
							wordIndexInComponent);
					System.out.println("summation for " + word.getWord()
							+ " ~ " + s_current);
					generateAndStoreSummations(index, first, second, c_current,
							s_current, wordIndex, result);

					frequencySummationDigits.add(s_current);
				}

				// queue the new frequency summation digits for one synset of a current word
				frequencyDigitsQueue.offer(frequencySummationDigits);
				// then resort it by size
				Collections.sort(frequencyDigitsQueue, queueSizeSorter);
			}
			else
			{
				// first is the last final one in the queue
				// put it back into the queue for step 5's usage
				frequencyDigitsQueue.offer(first);
				break;
			}
		}

		return result;
	}

	private void generateAndStoreSummations(int index, IntList first,
			IntList second, int c_current, int s_current, WordIndex wordIndex,
			Map<int[], Index> result)
	{
		if (index == 0)
		{
			// DO NOT use c_current since c_0 = '0'
			int x_0 = first.get(0);
			int y_0 = second.get(0);
			generateAndStoreFirstSummation(x_0, y_0, s_current, wordIndex,
					result);
		}
		else if (index < first.size())
		{
			Assert.isTrue(c_current != 0);
			int x_current = first.get(index);
			int y_current = second.get(index);
			generateAndStoreTwoAddendsSummation(x_current, y_current,
					c_current, s_current, wordIndex, result);
		}
		else if (index < second.size())
		{
			Assert.isTrue(c_current != 0);
			int y_current = second.get(index);
			generateAndStoreOneAddendSummation(y_current, c_current, s_current,
					wordIndex, result);
		}
		else
		{
			Assert.isTrue(c_current != 0);
			generateAndStoreLastSummation(c_current, s_current, wordIndex,
					result);

		}

	}

	/**
	 * s_0
	 * @param wordIndex 
	 */
	private void generateAndStoreFirstSummation(int x_0, int y_0, int s_0,
			WordIndex wordIndex, Map<int[], Index> result)
	{
		System.out.println("Step 4 summation ================================");
		// 1st half expression
		SortedAddArrayList firstHalfExpressionInDnf = new SortedAddArrayList();
		firstHalfExpressionInDnf.add(new int[] { not(s_0) });
		firstHalfExpressionInDnf.add(new int[] { not(x_0), y_0 });
		firstHalfExpressionInDnf.add(new int[] { x_0, not(y_0) });
		System.out.println("DNF ================");
		for (int[] each : firstHalfExpressionInDnf)
		{
			System.out.println(Arrays.toString(each));
		}

		List<int[]> firstHalfExpressionInCnf = convertDnfToCnf(firstHalfExpressionInDnf);
		Map<int[], Index> firstHalfExpressionInCnfMap = new HashMap<int[], SatIndexParser.Index>(
				firstHalfExpressionInCnf.size());
		System.out.println("CNF ================");
		for (int[] each : firstHalfExpressionInCnf)
		{
			firstHalfExpressionInCnfMap.put(each, wordIndex);
			System.out.println(Arrays.toString(each));
		}
		System.out.println("====================");

		firstHalfExpressionInCnf = null;
		result.putAll(firstHalfExpressionInCnfMap);

		// 2nd half expression
		int[] cnfClause = null;

		cnfClause = new int[] { s_0, x_0, not(y_0) };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { s_0, not(x_0), y_0 };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		System.out.println("Step 4 summation ================================");
	}

	private void generateAndStoreTwoAddendsSummation(int x_current,
			int y_current, int c_current, int s_current, WordIndex wordIndex,
			Map<int[], Index> result)
	{
		System.out.println("Step 4 summation ================================");
		// 1st half expression
		SortedAddArrayList firstHalfExpressionInDnf = new SortedAddArrayList();
		firstHalfExpressionInDnf.add(new int[] { not(s_current) });
		firstHalfExpressionInDnf.add(new int[] { not(x_current),
				not(y_current), c_current });
		firstHalfExpressionInDnf.add(new int[] { not(x_current), y_current,
				not(c_current) });
		firstHalfExpressionInDnf.add(new int[] { x_current, not(y_current),
				not(c_current) });
		firstHalfExpressionInDnf.add(new int[] { x_current, y_current,
				c_current });
		System.out.println("DNF ================");
		for (int[] each : firstHalfExpressionInDnf)
		{
			System.out.println(Arrays.toString(each));
		}

		List<int[]> firstHalfExpressionInCnf = convertDnfToCnf(firstHalfExpressionInDnf);
		Map<int[], Index> firstHalfExpressionInCnfMap = new HashMap<int[], SatIndexParser.Index>(
				firstHalfExpressionInCnf.size());
		System.out.println("CNF ================");
		for (int[] each : firstHalfExpressionInCnf)
		{
			firstHalfExpressionInCnfMap.put(each, wordIndex);
			System.out.println(Arrays.toString(each));
		}
		System.out.println("====================");

		firstHalfExpressionInCnf = null;
		result.putAll(firstHalfExpressionInCnfMap);

		// 2nd half expression
		int[] cnfClause = null;

		cnfClause = new int[] { s_current, not(x_current), y_current, c_current };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { s_current, x_current, not(y_current), c_current };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { s_current, x_current, y_current, not(c_current) };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { s_current, not(x_current), not(y_current),
				not(c_current) };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		System.out.println("Step 4 summation ================================");
	}

	private void generateAndStoreOneAddendSummation(int y_current,
			int c_current, int s_current, WordIndex wordIndex,
			Map<int[], Index> result)
	{
		System.out.println("Step 4 summation ================================");
		// 1st half expression
		SortedAddArrayList firstHalfExpressionInDnf = new SortedAddArrayList();
		firstHalfExpressionInDnf.add(new int[] { not(s_current) });
		firstHalfExpressionInDnf.add(new int[] { not(y_current), c_current });
		firstHalfExpressionInDnf.add(new int[] { y_current, not(c_current) });
		System.out.println("DNF ================");
		for (int[] each : firstHalfExpressionInDnf)
		{
			System.out.println(Arrays.toString(each));
		}
		List<int[]> firstHalfExpressionInCnf = convertDnfToCnf(firstHalfExpressionInDnf);
		Map<int[], Index> firstHalfExpressionInCnfMap = new HashMap<int[], SatIndexParser.Index>(
				firstHalfExpressionInCnf.size());
		System.out.println("CNF ================");
		for (int[] each : firstHalfExpressionInCnf)
		{
			firstHalfExpressionInCnfMap.put(each, wordIndex);
			System.out.println(Arrays.toString(each));
		}
		System.out.println("====================");

		firstHalfExpressionInCnf = null;
		result.putAll(firstHalfExpressionInCnfMap);

		// 2nd half expression
		int[] cnfClause = null;

		cnfClause = new int[] { s_current, not(y_current), c_current };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { s_current, y_current, not(c_current) };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		System.out.println("Step 4 summation ================================");
	}

	private void generateAndStoreLastSummation(int c_current, int s_current,
			WordIndex wordIndex, Map<int[], Index> result)
	{
		System.out.println("Step 4 summation ================================");

		int[] cnfClause = null;

		cnfClause = new int[] { s_current, not(c_current) };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { not(s_current), c_current };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		System.out.println("Step 4 summation ================================");
	}

	//////////////////////////////////

	// For carries: 	  1, 2, 3, ..., sizeOfFirst ~ total sizeOfFirst
	// addendIndex:    0, 1, 2, 3, ..., ..., ..., sizeOfSecond
	private void generateAndStoreCarries(int index, IntList first,
			IntList second, int c_previous, int c_current, WordIndex wordIndex,
			Map<int[], Index> result)
	{
		if (index == 1)
		{
			int x_0 = first.get(0);
			int y_0 = second.get(0);
			// DO NOT use c_previous here since c_0 = '0'!
			generateAndStoreFirstCarry(x_0, y_0, c_current, wordIndex, result);
		}
		else if (index <= first.size())
		{
			Assert.isTrue(c_previous != 0);
			int x_previous = first.get(index - 1);
			int y_previous = second.get(index - 1);

			generateAndStoreMiddleCarries(x_previous, y_previous, c_previous,
					c_current, wordIndex, result);
		}
		else
		{
			Assert.isTrue(c_previous != 0);
			int y_previous = second.get(index - 1);
			generateAndStoreLastCarry(y_previous, c_previous, c_current,
					wordIndex, result);
		}
	}

	private void generateAndStoreFirstCarry(int x_0, int y_0, int c_1,
			WordIndex wordIndex, Map<int[], Index> result)
	{
		System.out.println("Step 4 carry ====================================");

		// c_previous/c_0 equals to '0', so there's no c_0 variable
		int[] cnfClause = new int[] { not(c_1), x_0 };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { not(c_1), y_0 };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { c_1, not(x_0), not(y_0) };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		System.out.println("Step 4 carry ====================================");
	}

	private void generateAndStoreMiddleCarries(int x_previous, int y_previous,
			int c_previous, int c_current, WordIndex wordIndex,
			Map<int[], Index> result)
	{
		System.out.println("Step 4 carry ====================================");
		// 1st half expression
		SortedAddArrayList firstHalfExpressionInDnf = new SortedAddArrayList();
		firstHalfExpressionInDnf.add(new int[] { not(c_current) });
		firstHalfExpressionInDnf.add(new int[] { x_previous, y_previous });
		firstHalfExpressionInDnf.add(new int[] { x_previous, c_previous });
		firstHalfExpressionInDnf.add(new int[] { y_previous, c_previous });
		System.out.println("DNF ================");
		for (int[] each : firstHalfExpressionInDnf)
		{
			System.out.println(Arrays.toString(each));
		}
		List<int[]> firstHalfExpressionInCnf = convertDnfToCnf(firstHalfExpressionInDnf);
		Map<int[], Index> firstHalfExpressionInCnfMap = new HashMap<int[], SatIndexParser.Index>(
				firstHalfExpressionInCnf.size());
		System.out.println("CNF ================");
		for (int[] each : firstHalfExpressionInCnf)
		{
			firstHalfExpressionInCnfMap.put(each, wordIndex);
			System.out.println(Arrays.toString(each));
		}
		System.out.println("====================");

		firstHalfExpressionInCnf = null;
		result.putAll(firstHalfExpressionInCnfMap);

		// 2nd half expression
		int[] cnfClause = null;

		cnfClause = new int[] { not(x_previous), not(y_previous), c_current };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { not(x_previous), not(c_previous), c_current };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { not(y_previous), not(c_previous), c_current };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		System.out.println("Step 4 carry ====================================");
	}

	private void generateAndStoreLastCarry(int y_previous, int c_previous,
			int c_current, WordIndex wordIndex, Map<int[], Index> result)
	{
		System.out.println("Step 4 carry ====================================");
		int[] cnfClause = null;

		// 1st half expression
		cnfClause = new int[] { not(c_current), y_previous };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		cnfClause = new int[] { not(c_current), c_previous };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		// 2nd half expression
		cnfClause = new int[] { not(y_previous), not(c_previous), c_current };
		Arrays.sort(cnfClause);
		result.put(cnfClause, wordIndex);
		System.out.println(Arrays.toString(cnfClause));

		System.out.println("Step 4 carry ====================================");
	}

	////////////////////////////////////////////////////////////////////////////

	private Map<int[], Index> generateCnfForSummationLessThanOrEqualsToValue(
			Word word, IntList finalFrequencySummationDigits, int value)
	{
		int totalSummationDigitsNumber = finalFrequencySummationDigits.size();
		// NOTICE! reverse order!
		String valueBinaryString = StringUtils.reverse(Integer
				.toBinaryString(value));
		int valueBinaryStringLength = valueBinaryString.length();
		Assert.isTrue(
				totalSummationDigitsNumber >= valueBinaryStringLength,
				"The number of total ["
						+ totalSummationDigitsNumber
						+ "] bits for summation must greater than or equals to the number of bits for value["
						+ value + "(" + Integer.toBinaryString(value) + ")]. ");

		Map<int[], Index> greaterThanInCnf = generateCnfForSummationGreaterThanValue(
				word, finalFrequencySummationDigits, value);
		for (int[] eachClause : greaterThanInCnf.keySet())
		{
			for (int index = 0; index < eachClause.length; index++)
			{
				eachClause[index] = not(eachClause[index]);
			}
			Arrays.sort(eachClause);
		}

		List<int[]> notGreaterThanInDnf = new ArrayList<int[]>(
				greaterThanInCnf.keySet());
		List<int[]> notGreaterThanInCnf = convertDnfToCnf(notGreaterThanInDnf);

		greaterThanInCnf.clear();
		greaterThanInCnf = null;
		notGreaterThanInDnf.clear();
		notGreaterThanInDnf = null;

		WordIndex wordIndex = new WordIndex(component.getIndexOfWord(word), -1);
		Map<int[], Index> notGreaterThanInCnfMap = new HashMap<int[], Index>(
				notGreaterThanInCnf.size());

		System.out.println("Step 5 <" + value
				+ " =======================================");
		for (int[] each : notGreaterThanInCnf)
		{
			notGreaterThanInCnfMap.put(each, wordIndex);
			System.out.println(Arrays.toString(each));
		}
		System.out.println("Step 5 ==========================================");

		notGreaterThanInCnf = null;

		return notGreaterThanInCnfMap;

	}

	/**
	 *  -------------------
	 * |Step 5 in my report|
	 *  -------------------
	 * @param word 
	 *  
	 * @param finalFrequencySummationDigits
	 * @param value
	 * @return
	 */
	private Map<int[], Index> generateCnfForSummationGreaterThanValue(
			Word word, IntList finalFrequencySummationDigits, int value)
	{
		int totalSummationDigitsNumber = finalFrequencySummationDigits.size();
		// NOTICE! reverse order!
		String valueBinaryString = StringUtils.reverse(Integer
				.toBinaryString(value));
		int valueBinaryStringLength = valueBinaryString.length();
		Assert.isTrue(
				totalSummationDigitsNumber >= valueBinaryStringLength,
				"The number of bits for summation["
						+ totalSummationDigitsNumber
						+ "]bits must greater than or equals to the number of bits for value["
						+ value + "]. ");

		ArrayList<IntList> allCnfClauses = new ArrayList<IntList>();

		// drop first '1's
		int index = 0;
		while (index < valueBinaryStringLength
				&& valueBinaryString.charAt(index) == '1')
		{
			index++;
		}
		ArrayIntList intList = new ArrayIntList();
		allCnfClauses.add(intList);
		////////////////////////////////////////////////////////////////////////

		for (; index < totalSummationDigitsNumber; index++)
		{
			if (index < valueBinaryStringLength
					&& valueBinaryString.charAt(index) == '1')
			{
				intList = new ArrayIntList();
				intList.add(finalFrequencySummationDigits.get(index));
				allCnfClauses.add(intList);
			}
			else
			{
				for (IntList eachClause : allCnfClauses)
				{
					eachClause.add(finalFrequencySummationDigits.get(index));
				}
			}
		}

		WordIndex wordIndex = new WordIndex(component.getIndexOfWord(word), -1);
		Map<int[], Index> result = new TreeMap<int[], Index>(
				new IntArrayComparator());
		int[] clauseArray = null;
		System.out.println("Step 5 >" + value
				+ " =======================================");
		for (IntList clause : allCnfClauses)
		{
			clauseArray = clause.toArray();
			Arrays.sort(clauseArray);
			System.out.println(Arrays.toString(clauseArray));

			result.put(clauseArray, wordIndex);
		}
		System.out.println("Step 5 ==========================================");
		return result;
	}

	/*public static void main(String[] args)
	{
		AddingFrequencyCnfGeneratorImplKeepingMiddleVariables impl = new AddingFrequencyCnfGeneratorImplKeepingMiddleVariables(
				null);
		IntList finalFrequencySummationDigits = new ArrayIntList();
		finalFrequencySummationDigits.add(0);
		finalFrequencySummationDigits.add(1);
		finalFrequencySummationDigits.add(2);
		finalFrequencySummationDigits.add(3);

		for (int index = 0; index < 16; index++)
		{
			Collection<int[]> result = impl
					.generateCnfForSummationGreaterThanValue(
							finalFrequencySummationDigits, index);
			System.out.print(index + ": ");
			for (int[] each : result)
			{
				System.out.print(Arrays.toString(each) + " /\\ ");
			}

			result = impl.generateCnfForSummationLessThanOrEqualsToValue(
					finalFrequencySummationDigits, index);
			System.out.print("		");
			for (int[] each : result)
			{
				System.out.print(Arrays.toString(each) + " \\/ ");
			}

			System.out.println();
		}

		System.out.println("==============================================");
		SortedAddArrayList dnfs = new SortedAddArrayList();
		dnfs.add(new int[] { 0 });
		dnfs.add(new int[] { 1 });
		dnfs.add(new int[] { 2 });
		dnfs.add(new int[] { 3 });
		List<int[]> result = impl.convertDnfToCnf(dnfs);
		for (int[] each : result)
		{
			System.out.println(Arrays.toString(each));
		}
	}*/
}
